Narrowing is a procedure that was first studied in the context of equationalE-unification and that has been used in a wide range of applications. Theclassic completeness result due to Hullot states that any term rewritingderivation starting from an instance of an expression can be "lifted" to anarrowing derivation, whenever the substitution employed is normalized. In thispaper we adapt the generator- based extra-variables-elimination transformationused in functional-logic programming to overcome that limitation, so we areable to lift term rewriting derivations starting from arbitrary instances ofexpressions. The proposed technique is limited to left-linear constructorsystems and to derivations reaching a ground expression. We also present aMaude-based implementation of the technique, using natural rewriting for theon-demand evaluation strategy.
展开▼
